$\forall$$T$:Type, ${\it as}$:($T$ List). rev(${\it as}$) $\in$ ($T$ List)